Nuprl Lemma : es-axioms 11,40

the_es:event_system{i:l}. 
trans(es-E(the_es); e,e'.es-locl(the_esee'))
 SWellFounded(es-locl(the_esee'))
 (e,e':es-E(the_es).
 (loc(e) = loc(e' Id)  (es-locl(the_esee' (e = e' es-locl(the_ese'e)))
 (e:es-E(the_es). (es-first(the_ese))  (e':es-E(the_es). es-locl(the_ese'e)))
 (e:es-E(the_es). 
 ((es-first(the_ese)))
  (es-locl(the_es; es-pred(the_ese); e)
   (e':es-E(the_es). (es-locl(the_es; es-pred(the_ese); e' es-locl(the_ese'e)))))
 (e:es-E(the_es). 
 ((es-first(the_ese)))
  (x:Id, t:rationals.
  es_state_when(the_ese)(x,t)
  =
  es_state_after(the_es; es-pred(the_ese))
  (x
  ,t + (es-time(the_ese) - es-time(the_es; es-pred(the_ese))))
   es-vartype(the_es; loc(e); x)))
 trans(es-E(the_es); e,e'.es-causl(the_esee'))
 SWellFounded(es-causl(the_esee'))
 (e:es-E(the_es). 
 (es-isrcv(the_ese))
  (es-sends(the_es; es-lnk(the_ese); es-sender(the_ese))[es-index(the_ese)]
  (=
  (msg(es-lnk(the_ese); es-tag(the_ese); es-val(the_ese))
  ( es-Msg(the_es)))
 (e,e':es-E(the_es). es-locl(the_esee' es-causl(the_esee'))
 (e:es-E(the_es). (es-isrcv(the_ese))  es-causl(the_es; es-sender(the_ese); e))
 (e,e':es-E(the_es).
 es-causl(the_esee')
  ((((es-first(the_ese')))
  c (es-causl(the_ese; es-pred(the_ese'))  (e = es-pred(the_ese'))))
   ((es-isrcv(the_ese'))
   c (es-causl(the_ese; es-sender(the_ese'))  (e = es-sender(the_ese'))))))
 (e:es-E(the_es). (es-isrcv(the_ese))  (loc(e) = destination(es-lnk(the_ese))  Id))
 (e:es-E(the_es), l:IdLnk.
 ((loc(e) = source(l Id))  (es-sends(the_esle) = []  (es-Msgl(the_esl) List)))
 (e,e':es-E(the_es).
 (es-isrcv(the_ese))
  (es-isrcv(the_ese'))
  (es-lnk(the_ese) = es-lnk(the_ese' IdLnk)
  (es-locl(the_esee')
   (es-locl(the_es; es-sender(the_ese); es-sender(the_ese'))
    ((es-sender(the_ese) = es-sender(the_ese' es-E(the_es))
     (es-index(the_ese) < es-index(the_ese'))))))
 (e:es-E(the_es), l:IdLnk, n:int_seg(0; ||es-sends(the_esle)||).
 e':es-E(the_es)
 ((es-isrcv(the_ese'))
 c ((es-lnk(the_ese') = l)
 c  (es-sender(the_ese') = e)
 c  (es-index(the_ese') = n  )))) 
latex


Definitionsx:AB(x), es-E(es), es-locl(esee'), loc(e), es-first(ese), es-pred(ese), es-vartype(esix), es_state_when(ese), es_state_after(ese), es-time(ese), es-causl(esee'), es-isrcv(ese), es-Msg(es), es-index(ese), es-sends(esle), es-lnk(ese), es-sender(ese), es-tag(ese), es-val(ese), es-Msgl(esl), t.1, es_info(es), es-pred?(es), es-T(es), es_init(es), es-Trans(es), es_val(es), es_time(es), t.2, es-kind(ese), es-M(es), es-eq(es), es-oaxioms(es), t  T, event_system{i:l}, P  Q, A c B, EOrderAxioms(E;pred?;info)
Lemmasevent system wf

origin